package gov.nasa.jpf.symbc.modelcounter;

import java.util.Set;

import org.apfloat.Apfloat;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.symbc.numeric.PathCondition;

/**
 * The abstract class that forms the base class for all model counters. There is
 * no expectation that the model counter will use exact techniques to determine
 * of models that satisfy a path condition.
 */
public abstract class ModelCounter {

	/**
	 * Constructor for all model counters that extract the variable bounds from the given configuration.
	 * 
	 * @param config
	 *            a JPF configuration
	 */
	public ModelCounter(Config config) {
	}

	/**
	 * Return the condition probability that the given path condition is true.
	 * The path condition contains a "fresh" constraint C (the first constraint
	 * referenced by the {@link PathCondition#header} field), followed by the
	 * older path of the constraint D. This routine returns Pr(C | D). The
	 * probability Pr(D) is given by {@code parentProb}.
	 * 
	 * @param pathCondition
	 *            the path condition to evaluate
	 * @param parentProb
	 *            the probability that the older part of the constraint in the
	 *            path condition is true
	 * @return the probability that the path condition is true
	 */
	public abstract Apfloat getConditionalProbability(PathCondition pathCondition,
			Apfloat parentProb);

	/*
	 * Doing disjuncts
	 */
	public abstract Apfloat getProbability(Set<PathCondition> pathConditions);
	
	/**
	 * Report interesting statistics at end of run.
	 */
	public void report() {
	};

}
